Nowadays, the state-of-the-art model checking techniques are based on SAT (satisfiability) solvers. SAT solvers are less size sensitive than the formerly used BDDs (Binary Decision Diagrams) and capable to handle much larger designs. Therefore, many work in the area of model checking exploit the power of SAT solvers and integrate these techniques inside their algorithms.
SAT solver's task is to either find a satisfying assignment for a CNF (Conjunctive Normal Form) formula or to prove that one does not exist. This task is NP-complete. Therefore, a SAT solver is based on optimization and heuristics. In order to accelerate and enhance the power of a SAT solver, there are many works in the field of CNF simplification. These techniques perform semantic and syntactic reductions on the CNF formula in order ease the SAT solver's work in finding a satisfying assignment or to prove that one does not exist. Empirically, these simplification techniques significantly accelerate the run of the SAT solver, therefore, they are being used in many SAT-based techniques.
Another technique to cope the size problem in model checking is the use of abstractions. Abstraction techniques generate an abstract model that represents a super set of the states that are represented by the corresponding concrete model. Therefore, if one proved that a specification holds in an abstract model then the specification also holds in its corresponding concrete model. A representation of an abstract model is usually smaller than a representation of its corresponding concrete model therefore; it is easier to prove that a specification holds in an abstract model. However, due to the abstract states represented by the abstract model, the model checker may produce spurious counterexamples prove that the specification does not hold in the abstract model. For this reason, one can perform a refinement operation in order to discard some of the abstract states represented by the abstract model, this operation is called refinement and the general technique is called abstraction refinement.
SAT-based abstraction refinement model checking techniques are popular. These techniques combine two powerful methods that enable to verify specification on large and complicated designs. Therefore, the usage of SAT-based abstraction refinement techniques is common in the industry.
One of the options to accelerate SAT-based abstraction refinement techniques is by using a CNF simplifier as done in most other SAT-based techniques. However, integrating a CNF simplifier into the SAT-based abstraction refinement scheme is not straight forward due to the following reasons:                1. The simplification adds connections between variables that hurt the soundness of the refinement procedure.        2. Many refinement schemes work by building the formula gradually, and applying simplifications hurt the structural of the formula and destroy the ability to add the formula in a gradual and smart way.        